1. Technical Field
The present invention generally relates to verification techniques and in particular to verification techniques of digital integrated circuit designs.
2. Description of the Related Art
Digital design verification (where design verification is a way to verify that an integrated circuit (IC) design is correct) is a computationally expensive process; which generally requires resources that are exponential with respect to the size of the design under verification. Many prior art digital design verification algorithms rely on reachability analysis. Reachability analysis requires enumerating the reachable states (i.e. searching outward from the initial states in order to determine the set of states that are reachable) of the design under test to assess whether the design conforms to the required specification(s), which is a size-limited process. Reachable state set computation is at the core of many automatic formal verification techniques. However, current methods for the computation of reachable state set overapproximation are lossy (i.e. information pertaining to state reachability is lost since a state lying in an approximately reachable state set does not imply that the state is reachable), thereby including one or more states that are not reachable.
Multiple methods have been proposed for performing digital design verification that compute reachable state set overapproximation to avoid the computational complexity of precise reachable state computations. For example, a method has been developed for computing reachable state set overapproximation by deriving implication relationships between pairs of gates in a digital design. Although implication analysis generates tight reachability overapproximations, the main challenge for implication analysis is scalability. Implication derivation is more expensive for larger scale designs due to the number of candidate implication checks. The candidate implication checks are quadratic in the number of nodes required for the graph associated with the implication derivation; thereby resulting in expensive analysis. Methods have been proposed to represent the candidate implications in an implication graph and use transitive reduction to simplify the graph representation. The use of the implication graph has the advantage of enabling a large reduction in the number of candidate implication checks; however, the algorithms required for maintaining the transitive reduction of implication graphs are not cost effective.